Para trabajar con lógica de primer orden, vamos a utilizar el paquete nltk, y en particular su módulo de inferencia lógia y de construcción de modelos.
In [1]:
from nltk import *
In [2]:
from nltk.inference.resolution import *
Para leer una expresión utilizamos Expression.fromstring
, como lo vamos a utilizar mucho, le vamos a poner un nombre
all
y exists
segido de variable y un punto significan para todo y existe, respectivamente&
para el y, |
para el o, ->
para el implica, <->
para la equivalencia-
In [3]:
expr = Expression.fromstring
El comando skolemize
encuentra una forma normal de Skolem
In [4]:
e=expr("all x.S(x)->exist z.all y. R(x,y)")
skolemize(e)
Out[4]:
<OrExpression (-S(z1) | R(x,z2))>
Para reducir los contadores de las variables en esa expresión usamos normalize
In [5]:
_.normalize()
Out[5]:
<OrExpression (-S(z3) | R(z3,z3))>
In [6]:
e=expr("all x.(R(x,y)&-all y.R(x,y))")
In [7]:
s=skolemize(e).normalize()
In [8]:
print(s)
(R(z2,z1) & -R(z2,F4(z2)))
Dadas dos expresiones, most_general_unification
proporciona un unificador más general
La salida es un diccionario con la substitución
In [9]:
e1=expr("F(x,y)")
e2=expr("F(a,F(b))")
most_general_unification(e1,e2)
Out[9]:
{x: a, y: F(b)}
El comando Clause
aplicado a una lista de literales da como resultado una cláusula
In [10]:
Clause([e1,e2])
Out[10]:
{F(x,y), F(a,F(b))}
También podemos utilizar clausify
con una expresión obtenida previamente
Por ejemplo, si se lo aplicamos a $e=\forall x(R(x,y)\wedge \neg \forall y R(x,y))$, primero skolemiza y luego pasa a forma clausular
In [11]:
clausify(e)
Out[11]:
[{R(z9,z8)}, {-R(z10,F6(z10))}]
In [12]:
e=expr("all x.P(x)-> exists x.Q(x)")
clausify(e)
Out[12]:
[{-P(z13), Q(z14)}]
Existe un error que impide usar predicados sin variables con ciertos comandos, tal y como se ha informado aquí
In [13]:
e=expr("Q|-Q")
El comando skolemize(e)
, y por tanto clausify(e)
daría un error (que hemos omitido aquí)
Las cláusulas tienen un método que permite calcular resolventes
In [14]:
c1=Clause([expr("P(x)"),expr("Q(a)")])
c2=Clause([expr("-P(a)")])
In [15]:
c1
Out[15]:
{P(x), Q(a)}
In [16]:
c2
Out[16]:
{-P(a)}
In [17]:
c1.unify(c2)
Out[17]:
[{Q(a)}]
También podemos determinar si una cláusula es una tautología
In [18]:
c=clausify(expr("all x.(P(x)->P(x))"))
c
Out[18]:
[{-P(z16), P(z16)}]
In [19]:
c[0].is_tautology()
Out[19]:
True
O si una cláusula es subcláusula (subsume) a otra
In [20]:
Clause([expr("P(x)")]).subsumes(Clause([expr("P(x)"), expr("Q(A)")]))
Out[20]:
True
In [21]:
p1 = expr('humano(socrates)')
p2 = expr('all x.(humano(x) -> mortal(x))')
c = expr('mortal(socrates)')
print(p1,", ",p2,", ",c)
humano(socrates) , all x.(humano(x) -> mortal(x)) , mortal(socrates)
In [22]:
demostracion = ResolutionProverCommand(c, [p1,p2])
In [23]:
demostracion.prove()
Out[23]:
True
In [24]:
print(demostracion.proof())
[1] {-mortal(socrates)} A
[2] {humano(socrates)} A
[3] {-humano(z18), mortal(z18)} A
[4] {-humano(socrates)} (1, 3)
[5] {mortal(socrates)} (2, 3)
[6] {} (1, 5)
Esta demostración nos indica que los tres primeros pasos son elementos de $\{p_1, p_2,\neg c\}$, que [4] es resolvente de 1 y 3, que [5] lo es de 2 y 3, y que finalmente se obtiene la cláusula vacía como resolvente de 1 y 5
Veamos otro ejemplo, ahora con funciones
In [25]:
h1=expr("all y.-R(A,y)")
h2=expr("all x.(-Q(x)|R(x,F(x)))")
c=expr("-Q(A)")
In [26]:
demostracion = ResolutionProverCommand(c, [h1,h2])
In [27]:
demostracion.prove()
Out[27]:
True
In [28]:
print(demostracion.proof())
[1] {Q(A)} A
[2] {-R(A,z20)} A
[3] {-Q(z22), R(z22,F(z22))} A
[4] {R(A,F(A))} (1, 3)
[5] {-Q(A)} (2, 3)
[6] {} (1, 5)
Ejemplo con error
Veamos ahora un ejemplo más complicado: $$\{ \forall y(-C(y)\to \exists x A(x,y)), \forall x(\exists y(-C(y)\wedge A(x,y))\to M(x)), \forall x(D(x)\to M(x)), \forall x((M(x)\wedge D(x))\to \neg(\exists y(\neg C(y)\wedge A(x,y)))), \exists x\neg C(x)\}\models \exists x(M(x)\wedge \neg D(x)) $$
In [29]:
a=expr("exists x.(M(x)&-D(x))")
In [30]:
print(a)
exists x.(M(x) & -D(x))
In [31]:
h1=expr("all y.(-C(y)->exists x.A(x,y))")
h2=expr("all x.(exists y.(-C(y)&A(x,y))->M(x))")
h3=expr("all x.(D(x)->M(x))")
h4=expr("all x.((M(x)&D(x))->-(exists y.(-C(y)&A(x,y))))")
h5=expr("exists x.-C(x)")
In [32]:
demostracion = ResolutionProverCommand(a, [h1,h2,h3,h4,h5])
In [33]:
demostracion.prove()
Out[33]:
True
In [34]:
print(demostracion.proof())
[1] {-M(z24), D(z24)} A
[2] {C(z27), A(F25(z27),z27)} A
[3] {C(z30), -A(z31,z30), M(z31)} A
[4] {-D(z33), M(z33)} A
[5] {-M(z37), -D(z37), C(z36), -A(z37,z36)} A
[6] {-C(z39)} A
[7] {C(z30), -A(z31,z30), D(z31)} (1, 3)
[8] {} (1, 4)
Si observamos la demostración que nos proporciona este comando, vemos que de [1] y [4] ha obtenido la cláusula vacía, cosa que no es posible. Algo va mal. Veamos si podemos acotar mejor el error. Para ello tomemos el siguiente conjunto de fórmulas
In [35]:
h = Expression.fromstring("all x.(P(x) | Q(x))")
t= Expression.fromstring("all x.(-P(x) | -Q(x))")
s = Expression.fromstring("exists x.R(x)")
demostracion=ResolutionProverCommand(s,[h,t])
In [36]:
demostracion.prove()
Out[36]:
True
In [37]:
print(demostracion.proof())
[1] {-R(z41)} A
[2] {P(z43), Q(z43)} A
[3] {-P(z45), -Q(z45)} A
[4] {} (2, 3)
Una vez más vemos que deduce la cláusula vacía como resolvente de [2] y [3], lo cual no es posible
Veamos cómo hace la resolvente en estos casos
In [38]:
c=Clause([expr("P(x)"),expr("Q(x)")])
cn=Clause([expr("-P(x)"),expr("-Q(x)")])
In [39]:
c.unify(cn)
Out[39]:
[{}]
Lo cual es claramente erróneo
In [40]:
demostracion = TableauProverCommand(s,[h,t])
In [41]:
demostracion.prove()
Out[41]:
False
In [42]:
print(demostracion.proof())
-exists x.R(x)
all x.(-P(x) | -Q(x)): []
--> Using 'z46'
(-P(z46) | -Q(z46))
-P(z46)
all x.(-P(x) | -Q(x)): [z46]
--> Variables Exhausted
all x.-R(x): []
--> Using 'z46'
-R(z46)
all x.(-P(x) | -Q(x)): [z46]
--> Variables Exhausted
all x.-R(x): [z46]
--> Variables Exhausted
all x.(P(x) | Q(x)): []
--> Using 'z46'
(P(z46) | Q(z46))
P(z46)
CLOSED
Q(z46)
all x.(-P(x) | -Q(x)): [z46]
--> Variables Exhausted
all x.-R(x): [z46]
--> Variables Exhausted
all x.(P(x) | Q(x)): [z46]
--> Variables Exhausted
AGENDA EMPTY
In [43]:
h1=expr("all y.(-C(y)->exists x.A(x,y))")
h2=expr("all x.(exists y.(-C(y)&A(x,y))->M(x))")
h3=expr("all x.(D(x)->M(x))")
h4=expr("all x.((M(x)&D(x))->-(exists y.(-C(y)&A(x,y))))")
h5=expr("exists x.-C(x)")
a=expr("exists x.(M(x)&-D(x))")
In [44]:
demostracion = TableauProverCommand(a,[h1,h2,h3,h4,h5])
Por desgracia demostracion.prove()
demora más de lo deseado
In [45]:
h1=expr("all y.-R(A,y)")
h2=expr("all x.(-Q(x)|R(x,F(x)))")
c=expr("-Q(A)")
demostracion = TableauProverCommand(c,[h1,h2])
In [46]:
demostracion.prove()
---------------------------------------------------------------------------
RecursionError Traceback (most recent call last)
<ipython-input-46-bbe735c152ec> in <module>()
----> 1 demostracion.prove()
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/api.py in prove(self, verbose)
276 self._result, self._proof = self._prover._prove(self.goal(),
277 self.assumptions(),
--> 278 verbose)
279 return self._result
280
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _prove(self, goal, assumptions, verbose)
51 print(e)
52 else:
---> 53 raise e
54 return (result, '\n'.join(debugger.lines))
55
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _prove(self, goal, assumptions, verbose)
43 agenda.put_all(assumptions)
44 debugger = Debug(verbose)
---> 45 result = self._attempt_proof(agenda, set(), set(), debugger)
46 except RuntimeError as e:
47 if self._assume_false and str(e).startswith('maximum recursion depth exceeded'):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_d_neg(self, current, context, agenda, accessible_vars, atoms, debug)
185 def _attempt_proof_d_neg(self, current, context, agenda, accessible_vars, atoms, debug):
186 agenda.put(current.term.term, context)
--> 187 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
188
189 def _attempt_proof_n_all(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
215 new_agenda.put(current.second, context)
216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
--> 217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
219 def _attempt_proof_imp(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug)
102 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
103 agenda.mark_alls_fresh();
--> 104 return self._attempt_proof(agenda, accessible_vars|set(current.args), atoms|set([(current, False)]), debug+1)
105
106 def _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_or(self, current, context, agenda, accessible_vars, atoms, debug)
214 agenda.put(current.first, context)
215 new_agenda.put(current.second, context)
--> 216 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1) and \
217 self._attempt_proof(new_agenda, accessible_vars, atoms, debug+1)
218
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
--> 285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
286
287 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_n_atom(self, current, context, agenda, accessible_vars, atoms, debug)
118 #mark all AllExpressions as 'not exhausted' into the agenda since we are (potentially) adding new accessible vars
119 agenda.mark_alls_fresh();
--> 120 return self._attempt_proof(agenda, accessible_vars|set(current.term.args), atoms|set([(current.term, True)]), debug+1)
121
122 def _attempt_proof_prop(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
290 current._exhausted = True
291 agenda[Categories.ALL].add((current,context))
--> 292 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
293
294 else:
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof(self, agenda, accessible_vars, atoms, debug)
86
87 debug.line((current, context))
---> 88 return proof_method(current, context, agenda, accessible_vars, atoms, debug)
89
90 def _attempt_proof_atom(self, current, context, agenda, accessible_vars, atoms, debug):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in _attempt_proof_all(self, current, context, agenda, accessible_vars, atoms, debug)
281 debug.line('--> Using \'%s\'' % variable_to_use, 2)
282 current._used_vars |= set([variable_to_use])
--> 283 agenda.put(current.term.replace(current.variable, variable_to_use), context)
284 agenda[Categories.ALL].add((current,context))
285 return self._attempt_proof(agenda, accessible_vars, atoms, debug+1)
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/inference/tableau.py in put(self, expression, context)
371 else:
372 ex_to_add = expression
--> 373 self.sets[self._categorize_expression(ex_to_add)].add((ex_to_add, context))
374
375 def put_all(self, expressions):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __hash__(self)
941
942 def __hash__(self):
--> 943 return hash(repr(self))
944
945 def substitute_bindings(self, bindings):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __repr__(self)
1071
1072 def __repr__(self):
-> 1073 return '<%s %s>' % (self.__class__.__name__, self)
1074
1075 def __str__(self):
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1673
1674 def __str__(self):
-> 1675 return Tokens.NOT + "%s" % self.term
1676
1677
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in <genexpr>(.0)
1253 if self.is_atom():
1254 function, args = self.uncurry()
-> 1255 arg_str = ','.join("%s" % arg for arg in args)
1256 else:
1257 #Leave arguments curried
/Users/pedro/lib/anaconda/lib/python3.5/site-packages/nltk/sem/logic.py in __str__(self)
1383
1384 def __str__(self):
-> 1385 return "%s" % self.variable
1386
1387 class IndividualVariableExpression(AbstractVariableExpression):
RecursionError: maximum recursion depth exceeded while calling a Python object
Por suerte, nltk
ofrece una interfaz a prover9 que parece ser rápida y correcta
In [49]:
h1=expr("all y.(-C(y)->exists x.A(x,y))")
h2=expr("all x.(exists y.(-C(y)&A(x,y))->M(x))")
h3=expr("all x.(D(x)->M(x))")
h4=expr("all x.((M(x)&D(x))->-(exists y.(-C(y)&A(x,y))))")
h5=expr("exists x.-C(x)")
a=expr("exists x.(M(x)&-D(x))")
In [50]:
demostracion = Prover9Command(a,[h1,h2,h3,h4,h5])
In [51]:
demostracion.prove()
Out[51]:
True
In [52]:
print(demostracion.proof())
============================== prooftrans ============================
Prover9 (64) version 2009-11A, November 2009.
Process 30475 was started by pedro on MacBook-Pro-de-Pedro.local,
Thu May 12 17:52:50 2016
The command was "/Users/pedro/lib/LADR-2009-11A/bin/prover9".
============================== end of head ===========================
============================== end of input ==========================
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 17.
% Level of proof is 5.
% Maximum clause weight is 3.000.
% Given clauses 0.
1 (all x (-C(x) -> (exists y A(y,x)))). [assumption].
2 (all x ((exists y (-C(y) & A(x,y))) -> M(x))). [assumption].
4 (all x (M(x) & D(x) -> -(exists y (-C(y) & A(x,y))))). [assumption].
5 (exists x -C(x)). [assumption].
6 (exists x (M(x) & -D(x))). [goal].
7 -C(c1). [clausify(5)].
8 C(x) | A(f1(x),x). [clausify(1)].
9 C(x) | -A(y,x) | M(y). [clausify(2)].
10 -M(x) | -D(x) | C(y) | -A(x,y). [clausify(4)].
11 -M(x) | D(x). [deny(6)].
13 -M(x) | -D(x) | -A(x,c1). [resolve(7,a,10,c)].
14 -A(x,c1) | M(x). [resolve(7,a,9,a)].
15 A(f1(c1),c1). [resolve(7,a,8,a)].
16 -M(x) | -A(x,c1) | -M(x). [resolve(13,b,11,b)].
17 M(f1(c1)). [resolve(14,a,15,a)].
18 -M(f1(c1)) | -M(f1(c1)). [resolve(16,b,15,a)].
19 $F. [copy(18),merge(b),unit_del(a,17)].
============================== end of proof ==========================
Content source: pedritomelenas/LMD
Similar notebooks: